p:FinProbSpace, a, b:Atom2, C:p-open(p).
measure(C) = 1  (C:p-open(p)||a  C:p-open(p)||b)  (n:. (C(<n, random(p;a;b)>) = 1)) 

latex

Definitions	x:A. B(x), P  Q, P  Q, x:A. B(x), , t  T, A  B, {i..j}, S  T, suptype(S; T), i  j < k, P & Q, A, , p-open(p)
Lemmas	find-random wf, random wf, false wf, le wf, p-outcome wf, nat wf, free-from-atom wf2, p-open wf, p-open-measure-one wf, finite-prob-space wf